Search for: All records

The effectiveness of satisfiability solvers strongly depends on the quality of the encoding of a given problem into conjunctive normal form. Cardinality constraints are prevalent in numerous problems, prompting the development and study of various types of encoding. We present a novel approach to optimizing cardinality constraint encodings by exploring the impact of literal orderings within the constraints. By strategically placing related literals nearby each other, the encoding generates auxiliary variables in a hierarchical structure, enabling the solver to reason more abstractly about groups of related literals. Unlike conventional metrics such as formula size or propagation strength, our method leverages structural properties of the formula to redefine the roles of auxiliary variables to enhance the solver's learning capabilities. The experimental evaluation on benchmarks from the maximum satisfiability competition demonstrates that literal orderings can be more influential than the choice of the encoding type. Our literal ordering technique improves solver performance across various encoding techniques, underscoring the robustness of our approach. 

Abstract Duplex telomere binding proteins exhibit considerable structural and functional diversity in fungi. Herein we interrogate the activities and functions of two Myb-containing, duplex telomere repeat-binding factors inUstilago maydis, a basidiomycete that is evolutionarily distant from the standard fungi. These two telomere-binding proteins,UmTay1 andUmTrf2, despite having distinct domain structures, exhibit comparable affinities and sequence specificity for the canonical telomere repeats.UmTay1 specializes in promoting telomere replication and an ALT-like pathway, most likely by modulating the helicase activity of Blm.UmTrf2, in contrast, is critical for telomere protection; transcriptional repression ofUmtrf2leads to severe growth defects and profound telomere aberrations. Comparative analysis ofUmTay1 homologs in different phyla reveals broad functional diversity for this protein family and provides a case study for how DNA-binding proteins can acquire and lose functions at various chromosomal locations. Our findings also point to stimulatory effect of telomere protein on ALT inUstilago maydisthat may be conserved in other systems.